$\forall$$T$, ${\it T'}$:Type\{i\}, $f$:($T$$\rightarrow$${\it T'}$), $L$:($T$ List), $P$:(${\it T'}$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$\{i'\}).
\\[0ex]($\forall$$x$,$y$$\in$map($f$;$L$).  $P$($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($\forall$$x$,$y$$\in$$L$.  $P$($f$($x$),$f$($y$)))